$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow$prop\{i:l\}), $m$,$n$:$\mathbb{N}$, $x$,$y$,$z$:$T$.
\\[0ex]($x$ rel\_exp($T$; $R$; $m$) $y$) $\Rightarrow$ ($y$ rel\_exp($T$; $R$; $n$) $z$) $\Rightarrow$ ($x$ rel\_exp($T$; $R$; ($m$ + $n$)) $z$)